g:IAbMonoid, n:, a, b:|g|. (n  (a * b)) = ((n  a) * (n  b))  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, IAbMonoid
Definitions	False, A, A  B, i  j , P  Q, t  T, x:A. B(x), P & Q, P  Q, P  Q, x f y, , , IMonoid, IAbMonoid,
Lemmas	le wf, nat properties, grp car wf, iabmonoid wf, nat wf, mon ident, grp id wf, grp op wf, mon nat op zero, mon nat op unroll, abmonoid ac 1, mon assoc, mon nat op wf